\begin{tabbing}
$\forall$\=${\it es}$:ES, $T$:($i$:Id$\rightarrow$$k$:Knd$\rightarrow$kindtype($i$;$k$)$\rightarrow$es\_state(${\it es}$;$i$)$\rightarrow$es\_state(${\it es}$;$i$)),\+
\\[0ex]$S$:($i$:Id$\rightarrow$$k$:Knd$\rightarrow$kindtype($i$;$k$)$\rightarrow$state@$i$$\rightarrow$(Msg List)),
\\[0ex]$C$:($i$,$b$:Id$\rightarrow\mathbb{N}\rightarrow$state@$i$$\rightarrow$(?kindtype($i$;locl($b$)))).
\-\\[0ex](($\forall$$e$:E. (timed)state after $e$ = $T$(loc($e$),kind($e$),val($e$),es\_state\_when(${\it es}$;$e$)))
\\[0ex]\& (\=$\forall$$e$:E.\+
\\[0ex]($\uparrow$islocal(kind($e$)))
\\[0ex]$\Rightarrow$ ($\exists$\=$n$:$\mathbb{N}$\+
\\[0ex](($\uparrow$isl($C$(loc($e$),act(kind($e$)),$n$,(state when $e$))))
\\[0ex]c$\wedge$ (val($e$) = outl($C$(loc($e$),act(kind($e$)),$n$,(state when $e$))) $\in$ valtype($e$)))))
\-\-\\[0ex]\& (\=$\forall$$e$:E.\+
\\[0ex]($\uparrow$isrcv(kind($e$)))
\\[0ex]$\Rightarrow$ ($<$lnk(kind($e$)), tag(kind($e$)), val($e$)$>$ $\in$ \=$S$\+
\\[0ex](loc(sender($e$))
\\[0ex],kind(sender($e$))
\\[0ex],val(sender($e$))
\\[0ex],(state when sender($e$))))))
\-\-\\[0ex]$\Rightarrow$ \=($\forall$$a$:Atom1, $e$:E.\+
\\[0ex](\=$T$(loc($e$)):$k$:Knd$\rightarrow$kindtype(loc($e$);$k$)$\rightarrow$es\_state(${\it es}$;loc($e$))$\rightarrow$es\_state(${\it es}$;loc($e$))$\parallel$$a$\+
\\[0ex]$\Rightarrow$ $C$(loc($e$)):$b$:Id$\rightarrow\mathbb{N}\rightarrow$state@loc($e$)$\rightarrow$(?kindtype(loc($e$);locl($b$)))$\parallel$$a$
\\[0ex]$\Rightarrow$ ($\neg$($\uparrow$first($e$)))
\\[0ex]$\Rightarrow$ es\_state\_when(${\it es}$;pred($e$)):es\_state(${\it es}$;loc(pred($e$)))$\parallel$$a$
\\[0ex]$\Rightarrow$ (($\uparrow$isrcv(pred($e$))) $\Rightarrow$ val(pred($e$)):valtype(pred($e$))$\parallel$$a$)
\\[0ex]$\Rightarrow$ es\_state\_when(${\it es}$;$e$):es\_state(${\it es}$;loc($e$))$\parallel$$a$)
\-\\[0ex]\& (\=$S$(loc($e$)):$k$:Knd$\rightarrow$kindtype(loc($e$);$k$)$\rightarrow$state@loc($e$)$\rightarrow$(Msg List)$\parallel$$a$\+
\\[0ex]$\Rightarrow$ $C$(loc($e$)):$b$:Id$\rightarrow\mathbb{N}\rightarrow$state@loc($e$)$\rightarrow$(?kindtype(loc($e$);locl($b$)))$\parallel$$a$
\\[0ex]$\Rightarrow$ (state when $e$):state@loc($e$)$\parallel$$a$
\\[0ex]$\Rightarrow$ (($\uparrow$isrcv($e$)) $\Rightarrow$ val($e$):valtype($e$)$\parallel$$a$)
\\[0ex]$\Rightarrow$ $e$ sends $\parallel$ $a$))
\-\-
\end{tabbing}